\documentclass[10pt, conference, compsocconf]{IEEEtran}


\usepackage{array}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{colortbl}
\usepackage{hhline}
\usepackage{epsfig}
\usepackage{listings}
\usepackage{subfigure}
\usepackage{color}
\usepackage{epic,eepic}
\usepackage{url}
\usepackage{cite}
\usepackage{multirow}
\usepackage{graphicx}

%% \usepackage{listings}
%% \usepackage{subfigure}
%% \usepackage{epic,eepic}
%% \usepackage{url}
%% \usepackage{multirow}

\input{macros.tex}

% Add the compsocconf option for Computer Society conferences.
%
% If IEEEtran.cls has not been installed into the LaTeX system files,
% manually specify the path to it like:
% \documentclass[conference]{../sty/IEEEtran}
\begin{document}

%% \title{Efficient Model Checking of Data Races with
%%   \\ Automatically-extracted Distance-based Fitness Functions}

\title{Efficient Heuristic Model Checking of Data Races with
  \\ Specialized Fitness Functions}

% author names and affiliations
% use a multiple column layout for up to two different
% affiliations



\author{ 

  \IEEEauthorblockN{Jo\~ao Paulo Oliveira, Elton Alves, Marcelo
    d'Amorim, and Fernando Castor Filho}

  \IEEEauthorblockA{\textsuperscript{\dag}Federal University of
    Pernambuco, Brazil\\
    \texttt{\texttt{\{jpso,erma,damorim,castor\}@cin.ufpe.br}}}

}

\maketitle

\begin{abstract}
\Comment{Concurrency errors are easy to introduce and hard to find.}
Data races are a common kind of concurrency error that manifests when
two threads access shared data in an undisciplined order.
Heuristic-based model checking is a technique to systematically
explore the state-space of concurrent programs to find errors.  It
explores states in order defined by a heuristic function; this
function takes a program state as input and outputs its measure of
relevance.  One challenge of this approach is to find functions that
are not only precise (as to accurately identify relevant states) but
also efficient (as to reduce overall exploration time).  We propose
\tname{}, a technique that automates the extraction of a heuristic
function to guide the search for data race errors. It profiles the
model checker execution to identify potential conflicts on data and
with that information derives a heuristic function that guides the
rest of the state-space exploration.  We evaluated \tname{} on the
Java PathFinder (JPF) program model checker using subjects previously
used to evaluate race-finding techniques.  Our experimental results
indicate that \tname{} significantly reduces the number of states
explored until finding the first race and overall state-space
exploration time.
\end{abstract}

\begin{IEEEkeywords}
model checking, data races, fitness functions
\end{IEEEkeywords}


% For peer review papers, you can put extra information on the cover
% page as needed:
% \ifCLASSOPTIONpeerreview
% \begin{center} \bfseries EDICS Category: 3-BBND \end{center}
% \fi
%
% For peerreview papers, this IEEEtran command inserts a page break and
% creates the second title. It will be ignored for other modes.
%\IEEEpeerreviewmaketitle

\section{Introduction}

A common kind of concurrency error in shared-memory programs is a
\emph{data race} (or simply race).  The effect of a race is an
incorrect modification of state.  A race occurs when execution
contains two accesses to the same memory location that are \emph{not}
ordered by the happens-before relation~\cite{lamport1978} and at least
one of the accesses is a write.  Programmers prevent this from
happening by protecting potentially conflicting accesses to shared
data with at least one common lock\Comment{; this discipline assures
  the accesses are ordered}.  As in other kinds of concurrency errors,
data race typically manifests only in certain, often rare, thread
interleavings.  These interleavings are difficult to reproduce and
debug; hence it is important to help programmers find them.

Static and dynamic race detection tools have been previously proposed.
Static
tools~\cite{dwyer-clarke-fse94,flanagan-abadi-esop1999,boyapati-rinard-2001,agarwal-stoller-vmcai2004,naik-etal-pldi2006}
are ofen fast but can report false alarms; they make conservative
assumptions\Comment{\footnote{For example, for a language with
    pointers (or references), assumptions about possible pointer
    locations and, for an object-oriented language, assumptions about
    the types of targets of method invocations.}}  that accumulate and
tend to result in a large number of false positives.  Dynamic
tools~\cite{godefroid97:model,musuvathi02:cmc,visser03model,marino-etal-pldi2009,flanagan-freund-pldi2009},
on the other hand, typically don't report false alarms but they are
slower and can miss errors (e.g., due to an agressive space reduction
or due to a partial test driver).  This paper focuses on improving
dynamic tools; more precisely its search efficiency.

Program model
checking~\cite{godefroid97:model,musuvathi02:cmc,visser03model} is a
dynamic program analysis technique that helps users find concurrency
errors.  It systematically explores the space of possible thread
interleavings created with the execution of a test driver, which, in
this context, consists of a main function with operations to exercise
the subject under test (SUT).  Previous research has mainly focused on
reducing the combinatorial growth of the state
space~\cite{godefroid-por-book,clarke99:model,iosif02:symmetry}, which
is associated with the different choices of thread
interleavings\Comment{ and also to enabling efficient execution of
  code~\cite{?}}.

Our \emph{goal} is to speed up model-checking of the ``no data races''
property.  We want the model-checker to explore less states until
finding the first data-race.  The \emph{context} is of a model checker
that uses heuristic search to perform state-space exploration.  A
model checker of this kind uses a priority queue to store non-visited
states in order of their importance (/priorities), defined according
to an \Comment{ user-}informed fitness (/heuristic) function on state.
One challenge of this approach is to find a function that is both
useful (as to more precisely identify relevant states) and efficient
(as to reduce overall exploration time).  We conjecture that more
specialized functions helps in optimizing these goals.  Our
\emph{approach} is to infer from the SUT code a fitness function
specialized in data races for that given code.  The model checker uses
such a function to drive the state-space exploration towards regions
more likely to expose data races.

%%%%%% add later if we think stating assumption of the approach
%%%%%% explicitly is really necessary
\Comment{ This approach to model-checking~\cite{?,?,?} makes the
  following assumptions: (i) the fitness function are precise enough
  to drive the search to interesting states, (ii) the model checker
  finds bugs faster when focusing on states\Comment{ structurally}
  closer to suspicious regions, and that (iii) the additional cost of
  inferring the fitness function and evaluating fitness pays off.}

We propose \emph{\tname{}}, a technique to optimize model checking for
data races.  \tname{} operates in two stages.  In the first stage the
model checker simultaneously explores states and profiles execution in
search of opportunities to reaching a race.  The output of this stage
is a list of \emph{potential conflicts}.  In the second stage, the
model checker explores states guided by the potential race information
extracted in the previous stage.  The heuristic-function evaluates the
distance from a non-visited state to reach one potential conflict.

\Comment{
\Fix{not clear if we
  should add this =\gt{}} Decision when to transition from one stage
to another is determined by the income change of new information in
the first stage.}

\Comment{
  The goal of a state-space exploration in
this context is to cover the state that manifests the race.\Comment{
  that one potential conflict characterizes.}
}

Central in our approach is the dynamic discovery of potential race
conflicts.  One potential conflict consists of a pair of
thread-individual memory accesses characterizing the potential
scenario of a data race.  A key observation to justify \tname{} is
that during state-space exploration the model checker covers
\emph{individual} memory accesses much sooner than covering the actual
race.  For the experiments we considered, the model checker execution
identifies no distinct individual accesses after \Fix{N}\% of the
states are visited, on average.\Comment{what about new
  objects?}\Comment{ This information can be used to infer potential
  conflicts much sooner than the actual conflicts.\Fix{no false
    negatives} \Fix{what about false positives?}}  Also important is
that, in constrast to static analyses
input~\cite{findbugs-web-page,jlint-web-page}, the information
extracted during the profiling stage relates specific state entities
(e.g., threads, shared objects, and fields involved) enabling more
accurate identification of potential conflicts.\Comment{ Our approach
  uses this information to quickly infer a relatively small set of
  potential conflicts.}

\Comment { The technique infers suspicious regions from these accesses
  and updates the fitness functions accordingly.  }

\Comment{
Dynamic race finding tool typically require an exploration driver.
Heuristic search can improve the decisions of this driver about which
states to explore next.  
}

This paper makes the following contributions.

\mybull{Idea} We proposed a technique to optimize model checking for a
given goal.  The technique operates in two stages: one that profiles
execution in search of opportunities to reach the goal and the other
that performs a guided-search.
  
\mybull{Application} We instantiated the idea for the specific context
of finding data races in concurrent programs.  In this context, the
profiling stage looks for suspicious accesses to shared data.  We
observed that the profiler obtains precise information to guide the
search and that this information stabilizes relatively fast.

\mybull{Implementation} We implemented the technique on the
  Java PathFinder (JPF)~\cite{visser03model} program model checker.

\mybull{Experiment} We compared \tname{} with depth-first (DFS) and
breadth-first (BFS) explorations.  For that, we used several
applications from the Software-artifact Infrastructure Repository
(SIR)~\cite{doESE05} used previously to evaluate other bug-finding
techniques.  Our results indicate that \tname{} reduces on average the
number of states explored by \dfsStateReduction{} in DFS and by
\bfsStateReduction{} in BFS, on average.  It reduces time by
\dfsTimeReduction{} in DFS and by \bfsTimeReduction{} in BFS, on
average.

\section{Background}

Concurrent errors are notably easy to introduce and difficult to find,
specially in programs that follow a shared-memory programming
model~\cite{?}.  In such model, executing threads communicate by
reading and updating a shared space in memory.  Programmers need to
use some locking mechanism (e.g., monitors or semaphores) to protect
access to data, i.e., to prevent different threads from reading or
writing data inconsistently~\cite{?}.  The undisciplined use of locks
can result in blocking (e.g., deadlocks), lack of global progress
(livelocks) and incorrect state mutation (data races). 

We illustrate with one example the manifestation of a data race, which
is the error we focus in this paper.
Figure~\ref{fig:example:transfer} shows a fragment of a Java class
implementing a bank account.  The class \CodeIn{Account} has one field
to store the amount available in the account and a method to transfer
money between accounts.  The method \CodeIn{transfer} withdraws money
from the target account object (denoted by the \CodeIn{this}
reference) and deposits money in the account object passed as
parameter.  Note the use of modifier \CodeIn{synchronized} in the
declaration of \CodeIn{transfer}.  This has the effect of setting the
target account object (i.e., \CodeIn{this}) as the \emph{monitor} for
the method body; hence blocking any thread that attempts to execute a
block that is also protected by this monitor.  The semantic of Java
monitors is defined elsewhere~\cite{?}.

Unfortunately, the protection used in this example is not sufficient
to prevent race.  Figure~\ref{fig:example:race} shows a scenario where
two running threads call \CodeIn{transfer} on account objects
\CodeIn{acc1} and \CodeIn{acc2}.  One thread transfers money from
\CodeIn{acc1} to \CodeIn{acc2} and the other does the opposite.  To
simplify illustration we separate field reads in another statement
that reads the field and stores its value in the thread-local variable
\CodeIn{tmp}.  (This is similar to the way a JVM interprets the
bytecodes for this method.)  The problem in this example is that each
thread \emph{requests a different monitor} to access its critical
region.  The first requests monitor \CodeIn{acc1} and the second
requests monitor \CodeIn{acc2}.  As such no synchronization is in
effect: any interleaving is possible\footnote{This includes
  interleavings that violate sequential
  consistency~\cite{manson-etal-2005}.}.
Figure~\ref{fig:example:race} shows one particular scenario of race.
The second thread reads the values of \CodeIn{acc2.amount} first, then
the first thread executes to completion, and finally the second thread
resumes using the invalid value stored in the temporary.  Let use
assume that both accounts store 100 in the \CodeIn{amount} field.
This error results in the incorrect modification of
\CodeIn{acc2.amount} to 97 instead of 107.\Comment{ To fix this error
  one needs to use a common lock.}

%%%%%%%%%%%%  example subject
\lstset{escapeinside={\%*}{*)}}
\subfiguretopcaptrue
\begin{figure}[t]
  \centering
  \begin{small}
    \subfigure{
      \lstinputlisting[language=java,
      \Comment{numbers=left,numbersep=2pt,}basicstyle=\scriptsize]{Account.java}
    }
    \caption{\label{fig:example:transfer}Method
      \texttt{transfer}.} \figtabsep{}
    \vspace{-2ex}
  \end{small}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%  example race scheduling
\subfiguretopcaptrue
\begin{figure}[t]
 \centering
   \subfigure{
     \includegraphics[scale=0.7]{figs/transfer}
   }
   \caption{\label{fig:example:race}One scenario of race for the \texttt{Account}
     subject.  Each of the two columns in the figure shows the
     sequence of statements executed in one thread as result of a call
     to method \texttt{transfer}\Comment{ on two account objects}.  The spaces between
     statements indicate the choice of thread schedulings.}
   \figtabsep{}
\end{figure}
%%%%%%%%%%%% 

\Fix{a bit about program model checking. JPF, in particular.}

\section{Illustrative Example}

\Fix{...}

\section{Technique}

%% Joao, se vc. nao conseguiu compilar isto eh provavel que esteja
%% faltando algum pacote no seu ambiente (subfigure?).  de qualquer
%% forma, nao precisa comentar isto no seu commit.
\subfiguretopcaptrue
\begin{figure*}[t]
 \centering
   \subfigure{
     \includegraphics[scale=1.0]{figs/organization}
   }
   \caption{\label{fig:organization}Involved components in the
     implementation of proposed technique.} \figtabsep{}
\end{figure*}

\noindent\textbf{Overview.}The technique we propose is organized in
three parts: (i) profile of memory accesses during the execution of
the program model-checker, (ii) inference of suspicious regions of
data races from the profile data, and (iii) elaboration of fitness
function from these regions.  The profile data, the regions, and the
fitness function are updated when new information is observed during
the state-space exploration.  To avoid narrowing the search too early
the goal-driven search is only activated after profile data has
stabilized, i.e., the ratio of distinct memory accesses per number of
states visited in the state exploration reaches some defined lower
bound.

\Comment{The goal-driven search starts
after the model checker explores some defined number of states.}

\Comment{
automatically extract and use fitness functions specialized on data
races.  Extracted functions measure distance of a given state reached
by the model checker to regions of code more suspicious to contain
conflicting thread accesses to shared data.\Comment{ Ideally, fitter
  states are structurally closer to data race errors.}
}

\Comment{
To identify these
regions, we profile execution of the model checker and store relevant
information that can indicate possibility of conflicts.  

 For the experimental subjects we used, we
noticed that this information stabilizes very quickly (less than
\Fix{3}\% of total number of states explored) during the state-space
exploration and the cost of maintaining it is negligible.
}

\Comment{
Central in our approach is the extraction of a fitness function
specialized in data race errors.  Such function measures the
structural distance (in terms of distance in the call graph) of a
given state to a suspicious region.  }

\subsection{Profiler.}The profiler monitors, for each variable
access, the access kind (read or write), which threads share the
memory location involved, and the set of locks used to protect the
access.

\subsection{Likely Race Inferencer.}\Fix{...}

\subsection{Function generator.}\Fix{...}

\subfiguretopcaptrue
\begin{figure}[t]
  \centering
    \subfigure{
      \lstinputlisting[language=java,
      \Comment{numbers=left,numbersep=2pt,}basicstyle=\scriptsize]{Eval.java}
    }
    \caption{\label{algo:fitness-eval}Fitness evaluation.}
    \figtabsep{}
\end{figure}


\section{Evaluation}

This section presents the results of our evaluation.  We first show
subjects and setup of our experiments then show main results.  We
compared \tname{} with other search orders, evaluated the growth in
the number of potential conflicts discovered over time, and evaluated
the number of unconfirmed potential conflicts discovered (i.e., false
alarms).

\subsection{Subjects}
\label{sec:subjects}

We used subjects from the Software-artifact Infrastructure Repository
(SIR)~\cite{doESE05} previously used to evaluate race-finding
tools~\cite{?,?}.\Fix{...}

\begin{table*}[t]
\centering
\input{results}
\caption{\label{table:main}Comparison.}
\end{table*}

\subsection{Setup}
\label{sec:setup}

Our experiments used standard cofiguration of JPF but disabled the
\Fix{\CodeIn{jpf.report.abc}} parameter (set to \CodeIn{null}) so not
to generate trace data.  The use of tracing is helpful for debugging,
but singnificantly increases execution time.  This configuration
supports standard space-reduction techniques such as heap
symmetry~\cite{iosif:exploiting-heap-symmetries} and partial-order
reduction~\cite{godefroid-por-book}.  We compared \tname{} with
depth-first (DFS) and breadth-first (BFS) orders supported by JPF.
DFS order is JPF's default.

\subsection{Results}

\subsubsection{Search-space and time reduction}
\Fix{...}

\subsubsection{Growth of set of potential conflicts}
\Fix{...}

\subsubsection{Number unconfirmed potential conflicts}
\Fix{...}\Fix{may indicate that our approach can be used to guide
  inspection instead of reporting actual bugs.}

\subsection{Discussion}

To avoid errors related to the undisciplined use of locks other
concurrent-programming models and languages have been recently
proposed~\cite{?} and old models regained
force~\cite{lauterburg-etal-ase09}.  While these models and languages
do not become mainstream it is important to improve support for
existing models, specially considering the increasing demand for
software that runs on highly parallel multi-core machines that now
became more widespread.

\subsection{Threats to validity}

\Fix{Internal: implementation}

\Fix{External: subject (number of potential conflicts?  what if new
  allocated objects become shared?), other optimizations, other
  errors, etc.
}

\section{Related Work}

Recently, Marino~\etal{}~\cite{marino-etal-pldi2009} realized that
sampling could be very helpful to speed-up detection of data-races.
They selectively monitor thread accesses based on data obtained with
profiling.  Even though their goal is different, their fundamental
idea is similar to ours.  They recognize that not all points of
execution deserve same attention.  

Heuristic model checking has been investigated under different
contexts in the
past~\cite{groce02:model,rungta-mercer-haifa2008}.\Comment{ However,
  to the best of our knowledge, the use of specialized search
  heuristics has not been target of intensive research.}  Our
distinction from previous work is to focus specially on data races as
opposed to multiple kinds of concurrency errors and to obtain the
information of potential races with profiling as opposed to using the
output of tools such as FindBugs~\cite{findbugs-web-page} or
JLint~\cite{jlint-web-page}, which often report higher ratios of false
alarms~\cite{luo-etal-scam2010}.\Comment{, and to calculate distance
  of a state to potential conflic using dynamic data instead of
  statically, say using call graphs~\cite{rungta-mercer-haifa2008}.
  The use of call graphs can be problematic for dealing with call
  ordering and dynamic binding.}  We remain to compare Yoshi with the
input of static tools and also with other definition of distance
functions.

Previous dynamic analysis work focused on reducing cost of
instrumentation for efficient runtime
verification~\cite{schonberg-pldi1989,praun-gross-oopsla2001,pozniansky-schuster-2007,flanagan-freund-pldi2009,marino-etal-pldi2009},
and on improving precision of monitors~\cite{bodden-havelund-issta08}
that typically use variations of the Eraser lockset
algorithm~\cite{savage-etal-1997}.  These algorithms typically build
state machines to encode program states.  We remain to evaluate
whether \tname{} can leverage the distance to race states on these
state machines to adjust its measure of fitness.

\Fix{...Beverly Sanders work...}

\Comment{
The use of distance-based heursitic function was also used
recently by Rungta and Mercer~\cite{rungta-mercer-haifa2008}.  In
contrast, our distance function is based on dynamic instruction
distance as opposed to static function call distance.
}


\section{Conclusions}

\Fix{...}

\bibliographystyle{IEEEtranBST/IEEEtran}
\bibliography{testing}

\end{document}

% LocalWords:  livelocks multi interleavings FindBugs JLint Profiler profiler
% LocalWords:  Inferencer numbersep basicstyle Eval num DFS BFS yoshi improv
% LocalWords:  alarmClock lockset
